(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const i3 Int)
(assert (exists ((q0 Bool) (q1 Int) (q2 Int)) (=> (>= 118 q2) (=> q0 q0))))
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const i5 Int)
(assert (or (forall ((q11 Int) (q12 Bool) (q13 Int)) (not (not v14))) (exists ((q11 Int) (q12 Bool) (q13 Int)) (not (or (< 118 109) v0 q12 q12 v8 (distinct v13 v12 (<= 118 56)) v12 q12 v14 q12)))))
(declare-const v15 Bool)
(assert (not (forall ((q14 Bool) (q15 Bool)) v8)))
(assert (or (forall ((q14 Bool) (q15 Bool)) (not (or q14 q14 (= 118 i3)))) (exists ((q14 Bool) (q15 Bool)) (not (= q15 (= v9 v0 (xor v3 (= 118 i3) v9 v5 v9 (distinct v6 v12 v2 v3 v9 v0 (<= 118 56) v3) v4 v8 v8 (< 563 i2)) v6 (>= 118 (abs (- i2)))) v4 (>= 118 (abs (- i2))))))))
(declare-const v16 Bool)
(declare-const v17 Bool)
(assert (not (exists ((q16 Bool) (q17 Bool) (q18 Int) (q19 Bool)) (<= 118 56))))
(assert (or (forall ((q16 Bool) (q17 Bool) (q18 Int) (q19 Bool)) v11) (exists ((q16 Bool) (q17 Bool) (q18 Int) (q19 Bool)) (=> (and v3 v13 q16 v13 (distinct i5 765) (distinct i5 765) q16 q17 v2) (< q18 56)))))
(assert (exists ((q20 Bool) (q21 Bool)) (not (not (< 118 109)))))
(assert (not (exists ((q22 Int)) (not (distinct i1 q22)))))
(assert (forall ((q23 Int) (q24 Bool) (q25 Int)) (not (< q25 (- (mod i3 109) 986 (mod i3 109))))))
(check-sat)
